Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Enums #17

Closed
wants to merge 19 commits into from
Closed

Implement Enums #17

wants to merge 19 commits into from

Conversation

tillarnold
Copy link

@tillarnold tillarnold commented Nov 6, 2023

Replaced by #24


Builds on top of #16. To see what changed since #16 see https://github.com/tillarnold/prusti-dev/compare/rustfmt..tillarnold:prusti-dev:enum

This adds support for enums to new prusti, pure (snapshots) as well as impure (predicates).
I refactored mk_structlike to extract the different parts into functions that i can then reuse for mk_enum.

TODO:

  • test pure (currently not possible due to goto issue)
  • creating instances of enums in pure functions

@JonasAlaif
Copy link
Collaborator

This can't be used as is, please replay the changes without the cargo fmt once you have time :)

@tillarnold
Copy link
Author

@JonasAlaif with all the other changes that happened to the type encoder I'm not able to just replay the changes on the main branch. I will recreate this manually on top of the current branch without the fmt run but it'll take a bit more effort than just a rebase.

@tillarnold tillarnold closed this Nov 15, 2023
@tillarnold tillarnold mentioned this pull request Nov 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants